T:Type, P:(TProp), R1, R2:(TTProp).
when P, R1 => R2  R1 preserves P  (x, y:T. P(x)  (x (R1^*) y)  (x (R2^*) y)) 

latex

Definitions	when P, R1 => R2, R^*, x f y, R preserves P, Prop, t  T, x:A. B(x), P  Q
Lemmas	cond rel star monotone, cond rel implies wf, preserved by wf, rel star wf